% Appendix giving formal typing rules of NuSMV input language

\chapter{Typing Rules}
This appendix gives the explicit formal typing rules for {\nusmv}'s
input language, as well as notes on implicit conversion and casting.

In the following, an atomic constant is defined as being any sequence
of characters starting with a character in the set \code{\{A-Za-z\_\}}
and followed by a possible empty sequence of characters from the set
\code{\{A-Za-z0-9\_\$\#-$\backslash$\}}. An integer is any whole
number, positive or negative.

\section{Types}

The main types recognised by \nusmv are as follows:
\begin{itemize}
\item[] \Boolean 
\item[] \Integer 
\item[] \SymbEnum 
\item[] \IntSymbEnum 
\item[] \BoolSet
\item[] \IntSet 
\item[] \SymbSet 
\item[] \IntSymbSet 
\item[] \Word[N] (where \code{N} is any whole number $\geq$ 1)
%\item[] \WordArray[{[N][M]}] (where \code{N} and \code{M} are any whole number $\geq$ 1)
\end{itemize}

For more detalied description of existing types see \sref{Types}.
 
\section{Implicit Conversion}
In certain situations \nusmv is able to carry out implicit conversion
of types. There are two kind of implicit convertion. The first one
converts expression of one type to a greater type. The order to types 
is given in Figure~\ref{app_fig:typehierarchy}.
%
% This figure must be a copy from \sref{Type Order} !!!!!
\begin{figure}[h]
\begin{center}
\begin{tabular}{ccc}
      \begin{tabular}{cc}
	\Boolean\\
	$\downarrow$\\
	\Integer & \SymbEnum\\
	$\downarrow$ & $\downarrow$\\
	\multicolumn{2}{c}{\IntSymbEnum}\\
      \end{tabular} & &
%
      \begin{tabular}{c}
	\Word[1]\\
	\\
	\raisebox{1.3ex}[0pt]{~\Word[2]}\\
	\Word[3]\\
	\ldots \\
      \end{tabular} \\\\\\
%
      \begin{tabular}{cc}
	\BoolSet\\
	$\downarrow$\\
	\IntSet & \SymbSet\\
	$\downarrow$ & $\downarrow$\\
	\multicolumn{2}{c}{\IntSymbSet}\\
      \end{tabular} & &
%
%      \begin{tabular}{c}
%	\WordArray[{[1][1]}]\\
%	\\
%	\raisebox{1.3ex}[0pt]{~\WordArray[{[1][2]}]}\\
%	\WordArray[{[1][3]}]\\
%	\ldots \\
%      \end{tabular}
\end{tabular}
\end{center}
\caption{The ordering on the types in \nusmv\label{app_fig:typehierarchy}}
\end{figure}
For more information on type ordering see \sref{Implicit Type Conversion}.

Another kind of implicit type convertions changes the type of an
expression to its counterpart \Set type. The Figure~\ref{app_fig:set-type-cast} shows the
direction of such convertions.
%
% This figure must be consisten with description in \labe{Set Types}
\begin{figure}[h]
\begin{center}
\begin{tabular}{l}
 \Boolean $\rightarrow$ \BoolSet \\
\Integer $\rightarrow$ \IntSet \\
\SymbEnum $\rightarrow$ \SymbSet \\ 
 \IntSymbEnum $\rightarrow$ \IntSymbSet \\
\end{tabular}
\end{center}
\caption{Implicit convertion to counterpart \Set types\label{app_fig:set-type-cast}}
\end{figure}
For more information on \Set types and their counterpart types see
\sref{Set Types}.


\section{Type Rules}
The type rules are presented below with the operators on the left and
the signatures of the rules on the right. To save space, more than one
operator may be on the left-hand side, and it is also the case that an
individual operator may have more than one signature. For more information
on these expressions and their type rules see \sref{Expressions}.

\vspace{0.3in}

% Constants
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Constants}}\\
\hline
\multicolumn{2}{l}{~}\\
boolean\_constant & \Boolean\\
integer\_constant & \Integer\\
symbolic\_constant & \SymbEnum \\
word\_constant & \Word[N] (where \code{N} is the number of bits required)\\
range\_constant & \IntSet \\
\end{tabular}

\vspace{0.3in}

% Variable and Define
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Variable and Define}}\\
\hline
\multicolumn{2}{l}{~}\\
variable\_identifier & \code{Type} (where \code{Type} is the type of the variable)\\
define\_identifier & \code{Type} (where \code{Type} is the type of the define's expression)\\
\end{tabular}

\vspace{0.3in}

% Arithmetic Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Arithmetic Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
\code{-}  
 & \Boolean $\rightarrow$ \Integer\\
 & \Integer $\rightarrow$ \Integer\\
 & \Word[N] $\rightarrow$ \Word[N]\\
 \multicolumn{2}{r}{\qquad\footnotesize{The implicit type conversion can be applied
                    to the operand.}}\\

\code{+}, \code{-}, \code{/}, \code{*} 
 & \Boolean * \Boolean $\rightarrow$ \Integer\\
 & \Integer * \Integer $\rightarrow$ \Integer\\
 & \Word[N] * \Word[N] $\rightarrow$ \Word[N]\\
 \multicolumn{2}{r}{\qquad\footnotesize{The implicit type conversion can be applied
                    to \emph{one} of the operands.}}\\
\code{mod} 
 & \Integer * \textbf{2} $\rightarrow$ \Boolean\\
 & \Integer * \Integer $\rightarrow$ \Integer\\
 & \Word[N] * \Word[N] $\rightarrow$ \Word[N]\\
\multicolumn{2}{r}{\footnotesize{For operations on words, the result is
                   taken modulo $2^N$}}\\
\code{>}, \code{<}, \code{>=}, \code{<=} 
 & \Boolean * \Boolean $\rightarrow$ \Boolean\\
 & \Integer * \Integer $\rightarrow$ \Boolean\\
 & \Word[N] * \Word[N] $\rightarrow$ \Boolean\\
 & \Boolean * \Word[1] $\rightarrow$ \Boolean\\
 & \Word[1] * \Boolean $\rightarrow$ \Boolean\\
 \multicolumn{2}{r}{\qquad\footnotesize{The implicit type conversion can
                    be applied to \emph{one} of the operands.}}\\
\end{tabular}

\vspace{0.3in}

% Logic Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Logic Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
\code{!} (negation) 
 & \Boolean $\rightarrow$ \Boolean\\
 & \Word[N] $\rightarrow$ \Word[N]\\
\code{\&}, \code{|}, \code{->}, \code{<->}, \code{xor}, \code{xnor} 
 & \Boolean * \Boolean $\rightarrow$ \Boolean\\
 & \Word[N] * \Word[N] $\rightarrow$ \Word[N]\\
\code{=}, \code{!=} 
 & \Boolean * \Boolean $\rightarrow$ \Boolean\\
 & \Integer * \Integer $\rightarrow$ \Boolean\\
 & \SymbEnum * \SymbEnum $\rightarrow$ \Boolean\\
 & \IntSymbEnum * \\
   \multicolumn{2}{r}{\IntSymbEnum  $\rightarrow$ \Boolean}\\
 & \Word[N] * \Word[N] $\rightarrow$ \Boolean\\
% & \WordArray[{[N][M]}] * \WordArray[{[N][M]}] $\rightarrow$ \Boolean\\
 & \Boolean * \Word[1] $\rightarrow$ \Boolean\\
 & \Word[1] * \Boolean $\rightarrow$ \Boolean\\
 \multicolumn{2}{r}{\qquad\footnotesize{The implicit type conversion can
                    be applied to \emph{one} of the operands.}}\\
\end{tabular}

\vspace{0.3in}

% Bit-Wise Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Bit-Wise Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
\code{::} (concatenation) 
 & \Word[N] * \Word[M] $\rightarrow$ \Word[N+M]\\
 & \Boolean * \Word[N] $\rightarrow$ \Word[N+1]\\
 & \Word[N] * \Boolean $\rightarrow$ \Word[N+1]\\
\code{$exp_1$[$exp_2$, $exp_3$]} 
 & \Word[N] * \Integer * \Integer $\rightarrow$ \Word[$exp_3 - exp_2 + 1$]\\
\multicolumn{2}{l}{\qquad \footnotesize{exressions $exp_2$ and $exp_3$ must evaluate to integers such that 0 $\leq exp_2 \leq exp_3 <$ \code{N}}}\\
\code{<<}, \code{>>} (shift) 
 & \Word[N] * \Integer $\rightarrow$ \Word[N]\\
 & \Word[N] * \Boolean $\rightarrow$ \Word[N]\\
%\code{<<<}, \code{>>>} (rotation) & \Word[N] * \Integer $\rightarrow$ \Word[N]\\
%& \Word[N] * \Boolean $\rightarrow$ \Word[N]\\
\end{tabular}

\vspace{0.3in}

% Set Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Set Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
\code{\{$exp_1, exp_2, \ldots, exp_n$\}} & equivalent to consecutive \code{union} operations\\
\code{union} 
 &\BoolSet * \BoolSet $\rightarrow$ \BoolSet\\
 &\IntSet * \IntSet $\rightarrow$ \IntSet\\
 &\SymbSet * \SymbSet $\rightarrow$ \SymbSet\\
 &\IntSymbSet * \IntSymbSet \\
 \multicolumn{2}{r}{$\rightarrow$ \IntSymbSet}\\
 \multicolumn{2}{l}{\qquad \footnotesize{At first, if it is possible, the
              operands are converted to their \Set counterpart types,}}\\
 \multicolumn{2}{l}{\qquad \footnotesize{then both operands are implicitly
              converted to a minimal common type}}\\
\code{in} 
 &\BoolSet * \BoolSet $\rightarrow$ \BoolSet\\
 &\IntSet * \IntSet $\rightarrow$ \IntSet\\
 &\SymbSet * \SymbSet $\rightarrow$ \SymbSet\\
 &\IntSymbSet * \IntSymbSet \\
 \multicolumn{2}{r}{$\rightarrow$ \IntSymbSet}\\
 \multicolumn{2}{l}{\qquad \footnotesize{At first, if it is possible, the
               operands are converted to their \Set counterpart types,}}\\
 \multicolumn{2}{l}{\qquad \footnotesize{then implicit convertion is
                performed on one of the operands}}\\
\end{tabular}

\vspace{0.3in}

% Case Expression
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Case Expression}}\\
\hline
\multicolumn{2}{l}{~}\\
\code{case} & \code{$cond_1$ : $result_1$;}\\
& \code{$cond_2$ : $result_2$;}\\
& $\dots$\\
& \code{$cond_n$ : $result_n$;}\\
\code{esac}\\
\multicolumn{2}{l}{\qquad \footnotesize{\code{$cond_i$} must be of type
                   \Boolean. If one of \code{$result_i$} is of a \Set
                   type then all other \code{$result_k$} are}}\\
\multicolumn{2}{l}{\qquad \footnotesize{converted to their counterpart 
                   \Set types. The overall type of the expression is such
                   a minimal}}\\
\multicolumn{2}{l}{\qquad \footnotesize{type that each 
                   \code{$result_i$} can be implicitly converted to.}}\\
\end{tabular}

\vspace{0.3in}

% Formula Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Formula Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
\multicolumn{1}{l}{\code{EX}, \code{AX}, \code{EF}, \code{AF}, \code{EG}, \code{AG},}\\
\indent\code{X}, \code{Y}, \code{Z}, \code{G}, \code{H}, \code{F}, \code{O} 
 & \Boolean $\rightarrow$ \Boolean\\
\code{A-U}, \code{E-U}, \code{U}, \code{S} 
 & \Boolean * \Boolean $\rightarrow$ \Boolean\\
\code{A-BU}, \code{E-BU} 
 & \Boolean * \Integer * \Integer * \Boolean $\rightarrow$ \Boolean\\
\code{EBF}, \code{ABF}, \code{EBG}, \code{ABG} 
 & \Integer * \Integer * \Boolean $\rightarrow$ \Boolean\\
\end{tabular}

\vspace{0.3in}

% Miscellaneous Operators
\begin{tabular}{l@{ : }l}
\multicolumn{2}{l}{\textbf{Miscellaneous Operators}}\\
\hline
\multicolumn{2}{l}{~}\\
Integer\code{..}{Integer} 
 & \code{integer\_number} * \code{integer\_number} $\rightarrow$ \Integer\\
\code{bool}
 & \Word[1] $\rightarrow$ \Boolean\\
\code{word1} 
 & \Boolean $\rightarrow$ \Word[1]\\
\code{next}, \code{init} 
 & any type $\rightarrow$ the same type\\
\code{()} 
 & any type $\rightarrow$ the same type\\
\code{:=} 
 & \Boolean * \Boolean $\rightarrow$ no type\\
 & \Boolean * \BoolSet $\rightarrow$ no type\\
 & \Integer * \Integer $\rightarrow$ no type\\
 & \Integer * \IntSet $\rightarrow$ no type\\
 & \SymbEnum * \SymbEnum $\rightarrow$ no type\\
 & \SymbEnum * \SymbSet $\rightarrow$ no type\\
 & \IntSymbEnum * \\
   \multicolumn{2}{r}{\IntSymbEnum $\rightarrow$ no type}\\
 & \IntSymbEnum * \\
   \multicolumn{2}{r}{\IntSymbSet $\rightarrow$ no type}\\
 & \Word[N] * \Word[N] $\rightarrow$ no type\\
% & \WordArray[{[N][M]}] * \WordArray[{[N][M]}] $\rightarrow$ no type \\
 & \Boolean * \Word[1] $\rightarrow$ no type\\
 & \Word[1] * \Boolean $\rightarrow$ no type\\
\multicolumn{2}{l}{\footnotesize{Implicit type conversion is performed on the right operand only}}\\
\end{tabular}

